A:Type, B:(AType), f:fpf(A; a.B(a)), eq:EqDecider(A). fpf-join(eq; f; fpf-empty) = f 

latex

Definitions

x.A(x), <a, b>, (x  l), {x:A| B(x)} , f(a), x(s), x:AB(x), s = t, void, t  T, isect(A; x.B(x)), top, type List, x:A. B(x), subtype(S; T), [], append(as; bs), fpf-ap(f; eq; x), fpf-dom(eq; x; f), fpf-cap(f; eq; x; z), fpf-join(eq; f; g), fpf-empty, fpf(A; a.B(a)), x:A  B(x), Type, x. t(x), EqDecider(T), False, P  Q, A, b, prop{i:l}, b, , deq-member(eq; x; L), P  Q, P  Q, Unit, left + right, , if b then t else f fi

Lemmas

ifthenelse wf, it wf, unit wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bool wf, bnot wf, not wf, assert wf, deq wf, fpf wf, l member wf, append-nil, top wf